|
|
Akcelerace částicových rojů PSO pomocí GPU
Krézek, Vladimír ; Schwarz, Josef (oponent) ; Jaroš, Jiří (vedoucí práce)
Tato práce se zabývá technikou PSO (Particle Swarm Optimization neboli Optimalizace pomocí částicových rojů), s jejíž pomocí je možné řešit komplexní problémy. Tuto techniku lze využít při řešení složitých kombinatorických problémů (obchodní cestující, úloha o batohu), návrh integrovaných obvodů a antén, v oborech jako je biomedicína, robotika, umělá inteligence nebo i finančnictví. Přestože je algoritmus PSO velice efektivní, čas nezbytný pro nalezení vhodného řešení reálných problémů často přesahuje hranice únosnosti. Cílem této práce je tedy urychlit běh tohoto algoritmu pomocí grafického adaptéru, který nabízí velmi vysoký výpočetní potenciál při zachování příznivé ceny a rozměru. Pro demonstrační účely a ověření kvality implementace byl zvolen problém rozhodnutelnosti systému logických formulí (SAT), jenž patří do třídy NP-úplných problémů. Redukcí časové náročnosti algoritmu PSO při řešení SAT problému jsme tedy schopni akcelerovat celou třídu úloh a řešit problémy, které byly dosud prakticky neřešitelné.
|
|
|
Využití SAT solverů v úloze optimalizace kombinačních obvodů
Minařík, Vojtěch ; Mrázek, Vojtěch (oponent) ; Vašíček, Zdeněk (vedoucí práce)
Tato práce zavádí využití řešení problému SAT a jeho modifikací v úloze evolučního návrhu kombinačních obvodů. Motivací využití těchto problémů je zrychlení ohodnocování chromozomů kandidátních řešení fitness funkcí během evoluce v případech, kdy selhává metoda klasické simulace. Využití problému SAT, respektive #SAT umožňuje oproti simulaci zrychlení zejména pro komplikované obvody s velkým počtem vstupů. Implementované řešení se zalkádá právě na problému #SAT. Celkem byly implemenyovány dvě různé varianty využití tohoto problému. Varianty se liší metodou kontorly rozdílných hodnot na výstupech obvodu. Protože implementované řešení využívá k reprezentaci obvodu logickou formuli a zkoumá její splnitelnost, časová složitost algoritmu závisí především na logické složitosti navrhovaného obvodu.
|
|
|
Rozšíření matched formulí
Chromý, Miloš ; Kučera, Petr (vedoucí práce) ; Babka, Martin (oponent)
S KNF formulí můžeme asociovat incidenční graf. Tento graf je bipartitní a jedna partita zastupuje proměnné a druhá klauzule. Díky tomu můžeme definovat nové třídy KNF formulí, jimiž jsou matched formule a biklikově splnitelné formule. Obě tyto třídy mají tu vlastnost, že formule, které do nich patří jsou splnitelné i po změně polarity libovolného literálu. Takovým formulím říkáme var-splnitelné. V této práci uvažujeme práci Stefana Szeidera, která popisuje parametrizo- vaný algoritmus s pevným parametrem řešící problém matched formulí s malou deficiencí, což je rozdíl počtu klauzulí a počtu proměnných. Ukázali jsme, proč tento přístup nejde přímo zobecnit pro biklikově splnitelné formule. Vzhledem k tomu, že testování toho, je-li formule biklikově splnitelná, je NP- úplné, popsali jsme heuristiku, která hledá biklikové pokrytí v čase O(n2 e), kde n je počet proměnných ve formuli a e je délka formule. Provedli jsme experimenty na náhodných formulích. Z výsledků těchto experimentů lze usuzovat, že existuje fázový přechod ve výsledcích heuristiky. Dále jsme provedli experimenty, které ověřují existenci fázového přechodu matched formulí. Tyto výsledky jsme porov- nali s výsledky experimentů provedených s heuristikou. Výsledky experimentu provedeném na matched formulí jsme též porovnali s teoretickou hranicí...
|
|
|
Modelling and Solving Problems Using SAT Techniques
Balyo, Tomáš ; Barták, Roman (vedoucí práce) ; Železný, Filip (oponent) ; Biere, Armin (oponent)
Řešení problémů plánování prostřednictvím překladů do splnitelnosti (SAT) je jedním z nejúspěšnějších přístupů k automatickému plánování. V této práci popíšeme několik způsobů jak přeložit problém plánování reprezentovaný v SAS+ formalismu do SAT. Přezkoumáme a přizpůsobíme stávající kódování a také zavedeme nové vlastní způsoby kódování. Porovnáme jednotlivá kódování pomocí výpočtu horních odhadů na velikosti formulí, které produkují, a pomocí spuštění rozsáhlých experimentů na referenčních problémech z Mezinárodní plánovací soutěže 2011. V experimentální části také porovnáme své kódování s nejmodernejšími kódováními z plánovače Madagascar. Experimenty ukazují, že naše techniky dokažou překonat tato kódování. V předložené práci také řešíme speciální případ optimalizace plánů -- odstranění redundantních akcí. Odstranění všech redundantních akcí je NP- úplný problém. Prostudujeme existující polynomialní heuristické přístupy a navrhneme vlastní heuristický přístup, který dokaže eliminovat vyšší počet a dražší redundantní akce než stávající techniky. Také navrhneme způsob kódování problému redundance plánů do SAT, který nám za použití MaxSAT řešičů umožní optimálně vyřešit problém eliminace redundantních akcí. Naše experimenty provedené s plány od nejmodernejších satisficing plánovačů pro referenční problémy...
|
|
|
Multi-agent Path Finding
Švancara, Jiří ; Barták, Roman (vedoucí práce)
Zadáním multi-agentního hledání cest (MAPF z anglického multi-agent path finding) je nalézt nekonfliktní cesty pro neměnnou skupinu agentů, kteří se pohybují ve sdíleném prostředí. Každý z agentů je definován svojí výchozí a cílovou polohou. Tato běžná definice MAPF je velice jednoduchá a často nezohledňuje všechny parametry reálného světa, které je potřeba vyřešit, aby byl problém prakticky aplikovatelný. V této práci se snažíme tento nedostatek odstranit tím, že definici rozšíříme o několik parametrů. Toho dosáhneme v několika krocích. Nejprve představíme přístup k řešení MAPF pomocí převodu na splnitelnost Booleovských formulí. Tento přístup modelujeme v programovacím jazyce Picat, který nám poskytuje snadno upravitelný model, do kterého lze přidávat nové podmínky a omezení. Toho využijeme v dalším kroku, kdy upravíme původní zadání MAPF. Zaprvé povolíme, aby do sdíleného prostředí vstupovali noví agenti během exekuce již nalezeného plánu. Zadruhé relaxujeme požadavek na homogenitu sdíleného prostředí, které je běžně reprezentováno neohodnoceným grafem. V poslední části práce provedeme experimentální studii na skutečných robotech, abychom ověřili, že přidané atributy skutečně modelují situaci lépe než klasická definice.
|
|
|
Solving Boolean satisfiability problems
Balyo, Tomáš
V této práci studujeme možnosti rozkladu booleovských formulí do komponent souvislosti. Z tohoto důvodu zavádíme nový pojem - komponentový strom. Popisujeme některé vlastnosti komponentových stromů a možnosti jejich aplikace. Navrhli jsme třídu rozhodovacích heuristik pro SAT řešič na základě komponentových stromů a experimentálně zkoumali jejich výkon na testovacích SAT problémech. Pro tento účel jsme implementovali vlastní řešič, který využívá nejmodernější algoritmy a techniky pro řešení booleovské splnitelnosti.
|
|
|
Třídy Booleovských formulí s efektivně řešitelným SATem.
Vlček, Václav
Práce se zabývá třídami Booleovských formulí, pro které je problém splnitelnosti (SAT) řešitelný v polynomiálním čase. Zkoumá chování těchto tříd vzhledem k základním operacím s formulemi (komplementaci literálu, komplementaci proměnné, odebrání literálu nebo klauzule, částečné dosazení a spojení formulí). Dále se zabývá problémem rozpoznávání náležení formule do dané třídy, rozpoznávání splnitelnosti dané formule a vzájemnými vztahy těchto tříd vzhledem k inkluzi.
|
|
|
Multi-agent Path Finding
Švancara, Jiří ; Barták, Roman (vedoucí práce) ; Koenig, Sven (oponent) ; Vokřínek, Jiří (oponent)
Zadáním multi-agentního hledání cest (MAPF z anglického multi-agent path finding) je nalézt nekonfliktní cesty pro neměnnou skupinu agentů, kteří se pohybují ve sdíleném prostředí. Každý z agentů je definován svojí výchozí a cílovou polohou. Tato běžná definice MAPF je velice jednoduchá a často nezohledňuje všechny parametry reálného světa, které je potřeba vyřešit, aby byl problém prakticky aplikovatelný. V této práci se snažíme tento nedostatek odstranit tím, že definici rozšíříme o několik parametrů. Toho dosáhneme v několika krocích. Nejprve představíme přístup k řešení MAPF pomocí převodu na splnitelnost Booleovských formulí. Tento přístup modelujeme v programovacím jazyce Picat, který nám poskytuje snadno upravitelný model, do kterého lze přidávat nové podmínky a omezení. Toho využijeme v dalším kroku, kdy upravíme původní zadání MAPF. Zaprvé povolíme, aby do sdíleného prostředí vstupovali noví agenti během exekuce již nalezeného plánu. Zadruhé relaxujeme požadavek na homogenitu sdíleného prostředí, které je běžně reprezentováno neohodnoceným grafem. V poslední části práce provedeme experimentální studii na skutečných robotech, abychom ověřili, že přidané atributy skutečně modelují situaci lépe než klasická definice.
|
|
|
Využití SAT solverů v úloze optimalizace kombinačních obvodů
Minařík, Vojtěch ; Mrázek, Vojtěch (oponent) ; Vašíček, Zdeněk (vedoucí práce)
Tato práce zavádí využití řešení problému SAT a jeho modifikací v úloze evolučního návrhu kombinačních obvodů. Motivací využití těchto problémů je zrychlení ohodnocování chromozomů kandidátních řešení fitness funkcí během evoluce v případech, kdy selhává metoda klasické simulace. Využití problému SAT, respektive #SAT umožňuje oproti simulaci zrychlení zejména pro komplikované obvody s velkým počtem vstupů. Implementované řešení se zalkádá právě na problému #SAT. Celkem byly implemenyovány dvě různé varianty využití tohoto problému. Varianty se liší metodou kontorly rozdílných hodnot na výstupech obvodu. Protože implementované řešení využívá k reprezentaci obvodu logickou formuli a zkoumá její splnitelnost, časová složitost algoritmu závisí především na logické složitosti navrhovaného obvodu.
|
|
|
Rozšíření matched formulí
Chromý, Miloš ; Kučera, Petr (vedoucí práce) ; Babka, Martin (oponent)
S KNF formulí můžeme asociovat incidenční graf. Tento graf je bipartitní a jedna partita zastupuje proměnné a druhá klauzule. Díky tomu můžeme definovat nové třídy KNF formulí, jimiž jsou matched formule a biklikově splnitelné formule. Obě tyto třídy mají tu vlastnost, že formule, které do nich patří jsou splnitelné i po změně polarity libovolného literálu. Takovým formulím říkáme var-splnitelné. V této práci uvažujeme práci Stefana Szeidera, která popisuje parametrizo- vaný algoritmus s pevným parametrem řešící problém matched formulí s malou deficiencí, což je rozdíl počtu klauzulí a počtu proměnných. Ukázali jsme, proč tento přístup nejde přímo zobecnit pro biklikově splnitelné formule. Vzhledem k tomu, že testování toho, je-li formule biklikově splnitelná, je NP- úplné, popsali jsme heuristiku, která hledá biklikové pokrytí v čase O(n2 e), kde n je počet proměnných ve formuli a e je délka formule. Provedli jsme experimenty na náhodných formulích. Z výsledků těchto experimentů lze usuzovat, že existuje fázový přechod ve výsledcích heuristiky. Dále jsme provedli experimenty, které ověřují existenci fázového přechodu matched formulí. Tyto výsledky jsme porov- nali s výsledky experimentů provedených s heuristikou. Výsledky experimentu provedeném na matched formulí jsme též porovnali s teoretickou hranicí...
|
host ::
RSS.